The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^5).

(0) Obligation:

The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(1, n^5).


The TRS R consists of the following rules:

f_0(x) → a
f_1(x) → g_1(x, x)
g_1(s(x), y) → b(f_0(y), g_1(x, y))
f_2(x) → g_2(x, x)
g_2(s(x), y) → b(f_1(y), g_2(x, y))
f_3(x) → g_3(x, x)
g_3(s(x), y) → b(f_2(y), g_3(x, y))
f_4(x) → g_4(x, x)
g_4(s(x), y) → b(f_3(y), g_4(x, y))
f_5(x) → g_5(x, x)
g_5(s(x), y) → b(f_4(y), g_5(x, y))

Rewrite Strategy: INNERMOST

(1) TrsToWeightedTrsProof (BOTH BOUNDS(ID, ID) transformation)

Transformed TRS to weighted TRS

(2) Obligation:

The Runtime Complexity (innermost) of the given CpxWeightedTrs could be proven to be BOUNDS(1, n^5).


The TRS R consists of the following rules:

f_0(x) → a [1]
f_1(x) → g_1(x, x) [1]
g_1(s(x), y) → b(f_0(y), g_1(x, y)) [1]
f_2(x) → g_2(x, x) [1]
g_2(s(x), y) → b(f_1(y), g_2(x, y)) [1]
f_3(x) → g_3(x, x) [1]
g_3(s(x), y) → b(f_2(y), g_3(x, y)) [1]
f_4(x) → g_4(x, x) [1]
g_4(s(x), y) → b(f_3(y), g_4(x, y)) [1]
f_5(x) → g_5(x, x) [1]
g_5(s(x), y) → b(f_4(y), g_5(x, y)) [1]

Rewrite Strategy: INNERMOST

(3) TypeInferenceProof (BOTH BOUNDS(ID, ID) transformation)

Infered types.

(4) Obligation:

Runtime Complexity Weighted TRS with Types.
The TRS R consists of the following rules:

f_0(x) → a [1]
f_1(x) → g_1(x, x) [1]
g_1(s(x), y) → b(f_0(y), g_1(x, y)) [1]
f_2(x) → g_2(x, x) [1]
g_2(s(x), y) → b(f_1(y), g_2(x, y)) [1]
f_3(x) → g_3(x, x) [1]
g_3(s(x), y) → b(f_2(y), g_3(x, y)) [1]
f_4(x) → g_4(x, x) [1]
g_4(s(x), y) → b(f_3(y), g_4(x, y)) [1]
f_5(x) → g_5(x, x) [1]
g_5(s(x), y) → b(f_4(y), g_5(x, y)) [1]

The TRS has the following type information:

f_0 :: s → a:b a :: a:b f_1 :: s → a:b g_1 :: s → s → a:b s :: s → s b :: a:b → a:b → a:b f_2 :: s → a:b g_2 :: s → s → a:b f_3 :: s → a:b g_3 :: s → s → a:b f_4 :: s → a:b g_4 :: s → s → a:b f_5 :: s → a:b g_5 :: s → s → a:b

Rewrite Strategy: INNERMOST

(5) CompletionProof (UPPER BOUND(ID) transformation)

The transformation into a RNTS is sound, since:

(a) The obligation is a constructor system where every type has a constant constructor,

(b) The following defined symbols do not have to be completely defined, as they can never occur inside other defined symbols:

f_0
f_1
g_1
f_2
g_2
f_3
g_3
f_4
g_4
f_5
g_5

(c) The following functions are completely defined:
none

Due to the following rules being added:
none

And the following fresh constants:

const

(6) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: f_0(x) → a [1] f_1(x) → g_1(x, x) [1] g_1(s(x), y) → b(f_0(y), g_1(x, y)) [1] f_2(x) → g_2(x, x) [1] g_2(s(x), y) → b(f_1(y), g_2(x, y)) [1] f_3(x) → g_3(x, x) [1] g_3(s(x), y) → b(f_2(y), g_3(x, y)) [1] f_4(x) → g_4(x, x) [1] g_4(s(x), y) → b(f_3(y), g_4(x, y)) [1] f_5(x) → g_5(x, x) [1] g_5(s(x), y) → b(f_4(y), g_5(x, y)) [1] The TRS has the following type information: f_0 :: s → a:b a :: a:b f_1 :: s → a:b g_1 :: s → s → a:b s :: s → s b :: a:b → a:b → a:b f_2 :: s → a:b g_2 :: s → s → a:b f_3 :: s → a:b g_3 :: s → s → a:b f_4 :: s → a:b g_4 :: s → s → a:b f_5 :: s → a:b g_5 :: s → s → a:b const :: s Rewrite Strategy: INNERMOST

(7) NarrowingProof (BOTH BOUNDS(ID, ID) transformation)

Narrowed the inner basic terms of all right-hand sides by a single narrowing step.

(8) Obligation:

Runtime Complexity Weighted TRS where critical functions are completely defined. The underlying TRS is:

Runtime Complexity Weighted TRS with Types. The TRS R consists of the following rules: f_0(x) → a [1] f_1(x) → g_1(x, x) [1] g_1(s(x), y) → b(f_0(y), g_1(x, y)) [1] f_2(x) → g_2(x, x) [1] g_2(s(x), y) → b(f_1(y), g_2(x, y)) [1] f_3(x) → g_3(x, x) [1] g_3(s(x), y) → b(f_2(y), g_3(x, y)) [1] f_4(x) → g_4(x, x) [1] g_4(s(x), y) → b(f_3(y), g_4(x, y)) [1] f_5(x) → g_5(x, x) [1] g_5(s(x), y) → b(f_4(y), g_5(x, y)) [1] The TRS has the following type information: f_0 :: s → a:b a :: a:b f_1 :: s → a:b g_1 :: s → s → a:b s :: s → s b :: a:b → a:b → a:b f_2 :: s → a:b g_2 :: s → s → a:b f_3 :: s → a:b g_3 :: s → s → a:b f_4 :: s → a:b g_4 :: s → s → a:b f_5 :: s → a:b g_5 :: s → s → a:b const :: s Rewrite Strategy: INNERMOST

(9) CpxTypedWeightedTrsToRntsProof (UPPER BOUND(ID) transformation)

Transformed the TRS into an over-approximating RNTS by (improved) Size Abstraction.
The constant constructors are abstracted as follows:

a => 0
const => 0

(10) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: x >= 0, z = x
f_1(z) -{ 1 }→ g_1(x, x) :|: x >= 0, z = x
f_2(z) -{ 1 }→ g_2(x, x) :|: x >= 0, z = x
f_3(z) -{ 1 }→ g_3(x, x) :|: x >= 0, z = x
f_4(z) -{ 1 }→ g_4(x, x) :|: x >= 0, z = x
f_5(z) -{ 1 }→ g_5(x, x) :|: x >= 0, z = x
g_1(z, z') -{ 1 }→ 1 + f_0(y) + g_1(x, y) :|: x >= 0, y >= 0, z = 1 + x, z' = y
g_2(z, z') -{ 1 }→ 1 + f_1(y) + g_2(x, y) :|: x >= 0, y >= 0, z = 1 + x, z' = y
g_3(z, z') -{ 1 }→ 1 + f_2(y) + g_3(x, y) :|: x >= 0, y >= 0, z = 1 + x, z' = y
g_4(z, z') -{ 1 }→ 1 + f_3(y) + g_4(x, y) :|: x >= 0, y >= 0, z = 1 + x, z' = y
g_5(z, z') -{ 1 }→ 1 + f_4(y) + g_5(x, y) :|: x >= 0, y >= 0, z = 1 + x, z' = y

(11) InliningProof (UPPER BOUND(ID) transformation)

Inlined the following terminating rules on right-hand sides where appropriate:

f_0(z) -{ 1 }→ 0 :|: x >= 0, z = x

(12) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: x >= 0, z = x
f_1(z) -{ 1 }→ g_1(x, x) :|: x >= 0, z = x
f_2(z) -{ 1 }→ g_2(x, x) :|: x >= 0, z = x
f_3(z) -{ 1 }→ g_3(x, x) :|: x >= 0, z = x
f_4(z) -{ 1 }→ g_4(x, x) :|: x >= 0, z = x
f_5(z) -{ 1 }→ g_5(x, x) :|: x >= 0, z = x
g_1(z, z') -{ 2 }→ 1 + 0 + g_1(x, y) :|: x >= 0, y >= 0, z = 1 + x, z' = y, x' >= 0, y = x'
g_2(z, z') -{ 1 }→ 1 + f_1(y) + g_2(x, y) :|: x >= 0, y >= 0, z = 1 + x, z' = y
g_3(z, z') -{ 1 }→ 1 + f_2(y) + g_3(x, y) :|: x >= 0, y >= 0, z = 1 + x, z' = y
g_4(z, z') -{ 1 }→ 1 + f_3(y) + g_4(x, y) :|: x >= 0, y >= 0, z = 1 + x, z' = y
g_5(z, z') -{ 1 }→ 1 + f_4(y) + g_5(x, y) :|: x >= 0, y >= 0, z = 1 + x, z' = y

(13) SimplificationProof (BOTH BOUNDS(ID, ID) transformation)

Simplified the RNTS by moving equalities from the constraints into the right-hand sides.

(14) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 }→ g_1(z, z) :|: z >= 0
f_2(z) -{ 1 }→ g_2(z, z) :|: z >= 0
f_3(z) -{ 1 }→ g_3(z, z) :|: z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2 }→ 1 + 0 + g_1(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_2(z, z') -{ 1 }→ 1 + f_1(z') + g_2(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_3(z, z') -{ 1 }→ 1 + f_2(z') + g_3(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_4(z, z') -{ 1 }→ 1 + f_3(z') + g_4(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

(15) CpxRntsAnalysisOrderProof (BOTH BOUNDS(ID, ID) transformation)

Found the following analysis order by SCC decomposition:

{ f_0 } { g_1 } { f_1 } { g_2 } { f_2 } { g_3 } { f_3 } { g_4 } { f_4 } { g_5 } { f_5 }

(16) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 }→ g_1(z, z) :|: z >= 0
f_2(z) -{ 1 }→ g_2(z, z) :|: z >= 0
f_3(z) -{ 1 }→ g_3(z, z) :|: z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2 }→ 1 + 0 + g_1(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_2(z, z') -{ 1 }→ 1 + f_1(z') + g_2(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_3(z, z') -{ 1 }→ 1 + f_2(z') + g_3(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_4(z, z') -{ 1 }→ 1 + f_3(z') + g_4(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {f_0}, {g_1}, {f_1}, {g_2}, {f_2}, {g_3}, {f_3}, {g_4}, {f_4}, {g_5}, {f_5}

(17) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: f_0
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

(18) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 }→ g_1(z, z) :|: z >= 0
f_2(z) -{ 1 }→ g_2(z, z) :|: z >= 0
f_3(z) -{ 1 }→ g_3(z, z) :|: z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2 }→ 1 + 0 + g_1(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_2(z, z') -{ 1 }→ 1 + f_1(z') + g_2(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_3(z, z') -{ 1 }→ 1 + f_2(z') + g_3(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_4(z, z') -{ 1 }→ 1 + f_3(z') + g_4(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {f_0}, {g_1}, {f_1}, {g_2}, {f_2}, {g_3}, {f_3}, {g_4}, {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: ?, size: O(1) [0]

(19) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: f_0
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 1

(20) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 }→ g_1(z, z) :|: z >= 0
f_2(z) -{ 1 }→ g_2(z, z) :|: z >= 0
f_3(z) -{ 1 }→ g_3(z, z) :|: z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2 }→ 1 + 0 + g_1(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_2(z, z') -{ 1 }→ 1 + f_1(z') + g_2(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_3(z, z') -{ 1 }→ 1 + f_2(z') + g_3(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_4(z, z') -{ 1 }→ 1 + f_3(z') + g_4(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {g_1}, {f_1}, {g_2}, {f_2}, {g_3}, {f_3}, {g_4}, {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0]

(21) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(22) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 }→ g_1(z, z) :|: z >= 0
f_2(z) -{ 1 }→ g_2(z, z) :|: z >= 0
f_3(z) -{ 1 }→ g_3(z, z) :|: z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2 }→ 1 + 0 + g_1(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_2(z, z') -{ 1 }→ 1 + f_1(z') + g_2(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_3(z, z') -{ 1 }→ 1 + f_2(z') + g_3(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_4(z, z') -{ 1 }→ 1 + f_3(z') + g_4(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {g_1}, {f_1}, {g_2}, {f_2}, {g_3}, {f_3}, {g_4}, {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0]

(23) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: g_1
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

(24) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 }→ g_1(z, z) :|: z >= 0
f_2(z) -{ 1 }→ g_2(z, z) :|: z >= 0
f_3(z) -{ 1 }→ g_3(z, z) :|: z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2 }→ 1 + 0 + g_1(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_2(z, z') -{ 1 }→ 1 + f_1(z') + g_2(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_3(z, z') -{ 1 }→ 1 + f_2(z') + g_3(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_4(z, z') -{ 1 }→ 1 + f_3(z') + g_4(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {g_1}, {f_1}, {g_2}, {f_2}, {g_3}, {f_3}, {g_4}, {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: ?, size: O(1) [0]

(25) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: g_1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 2·z

(26) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 }→ g_1(z, z) :|: z >= 0
f_2(z) -{ 1 }→ g_2(z, z) :|: z >= 0
f_3(z) -{ 1 }→ g_3(z, z) :|: z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2 }→ 1 + 0 + g_1(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_2(z, z') -{ 1 }→ 1 + f_1(z') + g_2(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_3(z, z') -{ 1 }→ 1 + f_2(z') + g_3(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_4(z, z') -{ 1 }→ 1 + f_3(z') + g_4(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {f_1}, {g_2}, {f_2}, {g_3}, {f_3}, {g_4}, {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0]

(27) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(28) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 }→ g_2(z, z) :|: z >= 0
f_3(z) -{ 1 }→ g_3(z, z) :|: z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 1 }→ 1 + f_1(z') + g_2(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_3(z, z') -{ 1 }→ 1 + f_2(z') + g_3(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_4(z, z') -{ 1 }→ 1 + f_3(z') + g_4(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {f_1}, {g_2}, {f_2}, {g_3}, {f_3}, {g_4}, {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0]

(29) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: f_1
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

(30) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 }→ g_2(z, z) :|: z >= 0
f_3(z) -{ 1 }→ g_3(z, z) :|: z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 1 }→ 1 + f_1(z') + g_2(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_3(z, z') -{ 1 }→ 1 + f_2(z') + g_3(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_4(z, z') -{ 1 }→ 1 + f_3(z') + g_4(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {f_1}, {g_2}, {f_2}, {g_3}, {f_3}, {g_4}, {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: ?, size: O(1) [0]

(31) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: f_1
after applying outer abstraction to obtain an ITS,
resulting in: O(n¹) with polynomial bound: 1 + 2·z

(32) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 }→ g_2(z, z) :|: z >= 0
f_3(z) -{ 1 }→ g_3(z, z) :|: z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 1 }→ 1 + f_1(z') + g_2(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_3(z, z') -{ 1 }→ 1 + f_2(z') + g_3(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_4(z, z') -{ 1 }→ 1 + f_3(z') + g_4(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {g_2}, {f_2}, {g_3}, {f_3}, {g_4}, {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0]

(33) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(34) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 }→ g_2(z, z) :|: z >= 0
f_3(z) -{ 1 }→ g_3(z, z) :|: z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2 + 2·z' }→ 1 + s'' + g_2(z - 1, z') :|: s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 1 }→ 1 + f_2(z') + g_3(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_4(z, z') -{ 1 }→ 1 + f_3(z') + g_4(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {g_2}, {f_2}, {g_3}, {f_3}, {g_4}, {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0]

(35) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: g_2
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

(36) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 }→ g_2(z, z) :|: z >= 0
f_3(z) -{ 1 }→ g_3(z, z) :|: z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2 + 2·z' }→ 1 + s'' + g_2(z - 1, z') :|: s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 1 }→ 1 + f_2(z') + g_3(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_4(z, z') -{ 1 }→ 1 + f_3(z') + g_4(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {g_2}, {f_2}, {g_3}, {f_3}, {g_4}, {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0] g_2: runtime: ?, size: O(1) [0]

(37) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using CoFloCo for: g_2
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 2·z + 2·z·z'

(38) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 }→ g_2(z, z) :|: z >= 0
f_3(z) -{ 1 }→ g_3(z, z) :|: z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2 + 2·z' }→ 1 + s'' + g_2(z - 1, z') :|: s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 1 }→ 1 + f_2(z') + g_3(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_4(z, z') -{ 1 }→ 1 + f_3(z') + g_4(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {f_2}, {g_3}, {f_3}, {g_4}, {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0] g_2: runtime: O(n2) [2·z + 2·z·z'], size: O(1) [0]

(39) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(40) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 + 2·z + 2·z² }→ s1 :|: s1 >= 0, s1 <= 0, z >= 0
f_3(z) -{ 1 }→ g_3(z, z) :|: z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2·z + 2·z·z' }→ 1 + s'' + s2 :|: s2 >= 0, s2 <= 0, s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 1 }→ 1 + f_2(z') + g_3(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_4(z, z') -{ 1 }→ 1 + f_3(z') + g_4(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {f_2}, {g_3}, {f_3}, {g_4}, {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0] g_2: runtime: O(n2) [2·z + 2·z·z'], size: O(1) [0]

(41) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: f_2
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

(42) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 + 2·z + 2·z² }→ s1 :|: s1 >= 0, s1 <= 0, z >= 0
f_3(z) -{ 1 }→ g_3(z, z) :|: z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2·z + 2·z·z' }→ 1 + s'' + s2 :|: s2 >= 0, s2 <= 0, s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 1 }→ 1 + f_2(z') + g_3(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_4(z, z') -{ 1 }→ 1 + f_3(z') + g_4(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {f_2}, {g_3}, {f_3}, {g_4}, {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0] g_2: runtime: O(n2) [2·z + 2·z·z'], size: O(1) [0] f_2: runtime: ?, size: O(1) [0]

(43) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: f_2
after applying outer abstraction to obtain an ITS,
resulting in: O(n²) with polynomial bound: 1 + 2·z + 2·z²

(44) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 + 2·z + 2·z² }→ s1 :|: s1 >= 0, s1 <= 0, z >= 0
f_3(z) -{ 1 }→ g_3(z, z) :|: z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2·z + 2·z·z' }→ 1 + s'' + s2 :|: s2 >= 0, s2 <= 0, s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 1 }→ 1 + f_2(z') + g_3(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_4(z, z') -{ 1 }→ 1 + f_3(z') + g_4(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {g_3}, {f_3}, {g_4}, {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0] g_2: runtime: O(n2) [2·z + 2·z·z'], size: O(1) [0] f_2: runtime: O(n2) [1 + 2·z + 2·z2], size: O(1) [0]

(45) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(46) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 + 2·z + 2·z² }→ s1 :|: s1 >= 0, s1 <= 0, z >= 0
f_3(z) -{ 1 }→ g_3(z, z) :|: z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2·z + 2·z·z' }→ 1 + s'' + s2 :|: s2 >= 0, s2 <= 0, s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 2 + 2·z' + 2·z'² }→ 1 + s3 + g_3(z - 1, z') :|: s3 >= 0, s3 <= 0, z - 1 >= 0, z' >= 0
g_4(z, z') -{ 1 }→ 1 + f_3(z') + g_4(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {g_3}, {f_3}, {g_4}, {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0] g_2: runtime: O(n2) [2·z + 2·z·z'], size: O(1) [0] f_2: runtime: O(n2) [1 + 2·z + 2·z2], size: O(1) [0]

(47) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: g_3
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

(48) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 + 2·z + 2·z² }→ s1 :|: s1 >= 0, s1 <= 0, z >= 0
f_3(z) -{ 1 }→ g_3(z, z) :|: z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2·z + 2·z·z' }→ 1 + s'' + s2 :|: s2 >= 0, s2 <= 0, s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 2 + 2·z' + 2·z'² }→ 1 + s3 + g_3(z - 1, z') :|: s3 >= 0, s3 <= 0, z - 1 >= 0, z' >= 0
g_4(z, z') -{ 1 }→ 1 + f_3(z') + g_4(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {g_3}, {f_3}, {g_4}, {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0] g_2: runtime: O(n2) [2·z + 2·z·z'], size: O(1) [0] f_2: runtime: O(n2) [1 + 2·z + 2·z2], size: O(1) [0] g_3: runtime: ?, size: O(1) [0]

(49) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: g_3
after applying outer abstraction to obtain an ITS,
resulting in: O(n³) with polynomial bound: 2·z + 2·z·z' + 2·z·z'²

(50) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 + 2·z + 2·z² }→ s1 :|: s1 >= 0, s1 <= 0, z >= 0
f_3(z) -{ 1 }→ g_3(z, z) :|: z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2·z + 2·z·z' }→ 1 + s'' + s2 :|: s2 >= 0, s2 <= 0, s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 2 + 2·z' + 2·z'² }→ 1 + s3 + g_3(z - 1, z') :|: s3 >= 0, s3 <= 0, z - 1 >= 0, z' >= 0
g_4(z, z') -{ 1 }→ 1 + f_3(z') + g_4(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {f_3}, {g_4}, {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0] g_2: runtime: O(n2) [2·z + 2·z·z'], size: O(1) [0] f_2: runtime: O(n2) [1 + 2·z + 2·z2], size: O(1) [0] g_3: runtime: O(n3) [2·z + 2·z·z' + 2·z·z'2], size: O(1) [0]

(51) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(52) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 + 2·z + 2·z² }→ s1 :|: s1 >= 0, s1 <= 0, z >= 0
f_3(z) -{ 1 + 2·z + 2·z² + 2·z³ }→ s4 :|: s4 >= 0, s4 <= 0, z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2·z + 2·z·z' }→ 1 + s'' + s2 :|: s2 >= 0, s2 <= 0, s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 2·z + 2·z·z' + 2·z·z'² }→ 1 + s3 + s5 :|: s5 >= 0, s5 <= 0, s3 >= 0, s3 <= 0, z - 1 >= 0, z' >= 0
g_4(z, z') -{ 1 }→ 1 + f_3(z') + g_4(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {f_3}, {g_4}, {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0] g_2: runtime: O(n2) [2·z + 2·z·z'], size: O(1) [0] f_2: runtime: O(n2) [1 + 2·z + 2·z2], size: O(1) [0] g_3: runtime: O(n3) [2·z + 2·z·z' + 2·z·z'2], size: O(1) [0]

(53) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: f_3
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

(54) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 + 2·z + 2·z² }→ s1 :|: s1 >= 0, s1 <= 0, z >= 0
f_3(z) -{ 1 + 2·z + 2·z² + 2·z³ }→ s4 :|: s4 >= 0, s4 <= 0, z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2·z + 2·z·z' }→ 1 + s'' + s2 :|: s2 >= 0, s2 <= 0, s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 2·z + 2·z·z' + 2·z·z'² }→ 1 + s3 + s5 :|: s5 >= 0, s5 <= 0, s3 >= 0, s3 <= 0, z - 1 >= 0, z' >= 0
g_4(z, z') -{ 1 }→ 1 + f_3(z') + g_4(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {f_3}, {g_4}, {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0] g_2: runtime: O(n2) [2·z + 2·z·z'], size: O(1) [0] f_2: runtime: O(n2) [1 + 2·z + 2·z2], size: O(1) [0] g_3: runtime: O(n3) [2·z + 2·z·z' + 2·z·z'2], size: O(1) [0] f_3: runtime: ?, size: O(1) [0]

(55) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: f_3
after applying outer abstraction to obtain an ITS,
resulting in: O(n³) with polynomial bound: 1 + 2·z + 2·z² + 2·z³

(56) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 + 2·z + 2·z² }→ s1 :|: s1 >= 0, s1 <= 0, z >= 0
f_3(z) -{ 1 + 2·z + 2·z² + 2·z³ }→ s4 :|: s4 >= 0, s4 <= 0, z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2·z + 2·z·z' }→ 1 + s'' + s2 :|: s2 >= 0, s2 <= 0, s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 2·z + 2·z·z' + 2·z·z'² }→ 1 + s3 + s5 :|: s5 >= 0, s5 <= 0, s3 >= 0, s3 <= 0, z - 1 >= 0, z' >= 0
g_4(z, z') -{ 1 }→ 1 + f_3(z') + g_4(z - 1, z') :|: z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {g_4}, {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0] g_2: runtime: O(n2) [2·z + 2·z·z'], size: O(1) [0] f_2: runtime: O(n2) [1 + 2·z + 2·z2], size: O(1) [0] g_3: runtime: O(n3) [2·z + 2·z·z' + 2·z·z'2], size: O(1) [0] f_3: runtime: O(n3) [1 + 2·z + 2·z2 + 2·z3], size: O(1) [0]

(57) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(58) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 + 2·z + 2·z² }→ s1 :|: s1 >= 0, s1 <= 0, z >= 0
f_3(z) -{ 1 + 2·z + 2·z² + 2·z³ }→ s4 :|: s4 >= 0, s4 <= 0, z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2·z + 2·z·z' }→ 1 + s'' + s2 :|: s2 >= 0, s2 <= 0, s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 2·z + 2·z·z' + 2·z·z'² }→ 1 + s3 + s5 :|: s5 >= 0, s5 <= 0, s3 >= 0, s3 <= 0, z - 1 >= 0, z' >= 0
g_4(z, z') -{ 2 + 2·z' + 2·z'² + 2·z'³ }→ 1 + s6 + g_4(z - 1, z') :|: s6 >= 0, s6 <= 0, z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {g_4}, {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0] g_2: runtime: O(n2) [2·z + 2·z·z'], size: O(1) [0] f_2: runtime: O(n2) [1 + 2·z + 2·z2], size: O(1) [0] g_3: runtime: O(n3) [2·z + 2·z·z' + 2·z·z'2], size: O(1) [0] f_3: runtime: O(n3) [1 + 2·z + 2·z2 + 2·z3], size: O(1) [0]

(59) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: g_4
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

(60) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 + 2·z + 2·z² }→ s1 :|: s1 >= 0, s1 <= 0, z >= 0
f_3(z) -{ 1 + 2·z + 2·z² + 2·z³ }→ s4 :|: s4 >= 0, s4 <= 0, z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2·z + 2·z·z' }→ 1 + s'' + s2 :|: s2 >= 0, s2 <= 0, s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 2·z + 2·z·z' + 2·z·z'² }→ 1 + s3 + s5 :|: s5 >= 0, s5 <= 0, s3 >= 0, s3 <= 0, z - 1 >= 0, z' >= 0
g_4(z, z') -{ 2 + 2·z' + 2·z'² + 2·z'³ }→ 1 + s6 + g_4(z - 1, z') :|: s6 >= 0, s6 <= 0, z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {g_4}, {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0] g_2: runtime: O(n2) [2·z + 2·z·z'], size: O(1) [0] f_2: runtime: O(n2) [1 + 2·z + 2·z2], size: O(1) [0] g_3: runtime: O(n3) [2·z + 2·z·z' + 2·z·z'2], size: O(1) [0] f_3: runtime: O(n3) [1 + 2·z + 2·z2 + 2·z3], size: O(1) [0] g_4: runtime: ?, size: O(1) [0]

(61) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: g_4
after applying outer abstraction to obtain an ITS,
resulting in: O(n⁴) with polynomial bound: 2·z + 2·z·z' + 2·z·z'² + 2·z·z'³

(62) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 + 2·z + 2·z² }→ s1 :|: s1 >= 0, s1 <= 0, z >= 0
f_3(z) -{ 1 + 2·z + 2·z² + 2·z³ }→ s4 :|: s4 >= 0, s4 <= 0, z >= 0
f_4(z) -{ 1 }→ g_4(z, z) :|: z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2·z + 2·z·z' }→ 1 + s'' + s2 :|: s2 >= 0, s2 <= 0, s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 2·z + 2·z·z' + 2·z·z'² }→ 1 + s3 + s5 :|: s5 >= 0, s5 <= 0, s3 >= 0, s3 <= 0, z - 1 >= 0, z' >= 0
g_4(z, z') -{ 2 + 2·z' + 2·z'² + 2·z'³ }→ 1 + s6 + g_4(z - 1, z') :|: s6 >= 0, s6 <= 0, z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0] g_2: runtime: O(n2) [2·z + 2·z·z'], size: O(1) [0] f_2: runtime: O(n2) [1 + 2·z + 2·z2], size: O(1) [0] g_3: runtime: O(n3) [2·z + 2·z·z' + 2·z·z'2], size: O(1) [0] f_3: runtime: O(n3) [1 + 2·z + 2·z2 + 2·z3], size: O(1) [0] g_4: runtime: O(n4) [2·z + 2·z·z' + 2·z·z'2 + 2·z·z'3], size: O(1) [0]

(63) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(64) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 + 2·z + 2·z² }→ s1 :|: s1 >= 0, s1 <= 0, z >= 0
f_3(z) -{ 1 + 2·z + 2·z² + 2·z³ }→ s4 :|: s4 >= 0, s4 <= 0, z >= 0
f_4(z) -{ 1 + 2·z + 2·z² + 2·z³ + 2·z⁴ }→ s7 :|: s7 >= 0, s7 <= 0, z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2·z + 2·z·z' }→ 1 + s'' + s2 :|: s2 >= 0, s2 <= 0, s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 2·z + 2·z·z' + 2·z·z'² }→ 1 + s3 + s5 :|: s5 >= 0, s5 <= 0, s3 >= 0, s3 <= 0, z - 1 >= 0, z' >= 0
g_4(z, z') -{ 2·z + 2·z·z' + 2·z·z'² + 2·z·z'³ }→ 1 + s6 + s8 :|: s8 >= 0, s8 <= 0, s6 >= 0, s6 <= 0, z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0] g_2: runtime: O(n2) [2·z + 2·z·z'], size: O(1) [0] f_2: runtime: O(n2) [1 + 2·z + 2·z2], size: O(1) [0] g_3: runtime: O(n3) [2·z + 2·z·z' + 2·z·z'2], size: O(1) [0] f_3: runtime: O(n3) [1 + 2·z + 2·z2 + 2·z3], size: O(1) [0] g_4: runtime: O(n4) [2·z + 2·z·z' + 2·z·z'2 + 2·z·z'3], size: O(1) [0]

(65) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: f_4
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

(66) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 + 2·z + 2·z² }→ s1 :|: s1 >= 0, s1 <= 0, z >= 0
f_3(z) -{ 1 + 2·z + 2·z² + 2·z³ }→ s4 :|: s4 >= 0, s4 <= 0, z >= 0
f_4(z) -{ 1 + 2·z + 2·z² + 2·z³ + 2·z⁴ }→ s7 :|: s7 >= 0, s7 <= 0, z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2·z + 2·z·z' }→ 1 + s'' + s2 :|: s2 >= 0, s2 <= 0, s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 2·z + 2·z·z' + 2·z·z'² }→ 1 + s3 + s5 :|: s5 >= 0, s5 <= 0, s3 >= 0, s3 <= 0, z - 1 >= 0, z' >= 0
g_4(z, z') -{ 2·z + 2·z·z' + 2·z·z'² + 2·z·z'³ }→ 1 + s6 + s8 :|: s8 >= 0, s8 <= 0, s6 >= 0, s6 <= 0, z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {f_4}, {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0] g_2: runtime: O(n2) [2·z + 2·z·z'], size: O(1) [0] f_2: runtime: O(n2) [1 + 2·z + 2·z2], size: O(1) [0] g_3: runtime: O(n3) [2·z + 2·z·z' + 2·z·z'2], size: O(1) [0] f_3: runtime: O(n3) [1 + 2·z + 2·z2 + 2·z3], size: O(1) [0] g_4: runtime: O(n4) [2·z + 2·z·z' + 2·z·z'2 + 2·z·z'3], size: O(1) [0] f_4: runtime: ?, size: O(1) [0]

(67) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: f_4
after applying outer abstraction to obtain an ITS,
resulting in: O(n⁴) with polynomial bound: 1 + 2·z + 2·z² + 2·z³ + 2·z⁴

(68) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 + 2·z + 2·z² }→ s1 :|: s1 >= 0, s1 <= 0, z >= 0
f_3(z) -{ 1 + 2·z + 2·z² + 2·z³ }→ s4 :|: s4 >= 0, s4 <= 0, z >= 0
f_4(z) -{ 1 + 2·z + 2·z² + 2·z³ + 2·z⁴ }→ s7 :|: s7 >= 0, s7 <= 0, z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2·z + 2·z·z' }→ 1 + s'' + s2 :|: s2 >= 0, s2 <= 0, s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 2·z + 2·z·z' + 2·z·z'² }→ 1 + s3 + s5 :|: s5 >= 0, s5 <= 0, s3 >= 0, s3 <= 0, z - 1 >= 0, z' >= 0
g_4(z, z') -{ 2·z + 2·z·z' + 2·z·z'² + 2·z·z'³ }→ 1 + s6 + s8 :|: s8 >= 0, s8 <= 0, s6 >= 0, s6 <= 0, z - 1 >= 0, z' >= 0
g_5(z, z') -{ 1 }→ 1 + f_4(z') + g_5(z - 1, z') :|: z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0] g_2: runtime: O(n2) [2·z + 2·z·z'], size: O(1) [0] f_2: runtime: O(n2) [1 + 2·z + 2·z2], size: O(1) [0] g_3: runtime: O(n3) [2·z + 2·z·z' + 2·z·z'2], size: O(1) [0] f_3: runtime: O(n3) [1 + 2·z + 2·z2 + 2·z3], size: O(1) [0] g_4: runtime: O(n4) [2·z + 2·z·z' + 2·z·z'2 + 2·z·z'3], size: O(1) [0] f_4: runtime: O(n4) [1 + 2·z + 2·z2 + 2·z3 + 2·z4], size: O(1) [0]

(69) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(70) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 + 2·z + 2·z² }→ s1 :|: s1 >= 0, s1 <= 0, z >= 0
f_3(z) -{ 1 + 2·z + 2·z² + 2·z³ }→ s4 :|: s4 >= 0, s4 <= 0, z >= 0
f_4(z) -{ 1 + 2·z + 2·z² + 2·z³ + 2·z⁴ }→ s7 :|: s7 >= 0, s7 <= 0, z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2·z + 2·z·z' }→ 1 + s'' + s2 :|: s2 >= 0, s2 <= 0, s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 2·z + 2·z·z' + 2·z·z'² }→ 1 + s3 + s5 :|: s5 >= 0, s5 <= 0, s3 >= 0, s3 <= 0, z - 1 >= 0, z' >= 0
g_4(z, z') -{ 2·z + 2·z·z' + 2·z·z'² + 2·z·z'³ }→ 1 + s6 + s8 :|: s8 >= 0, s8 <= 0, s6 >= 0, s6 <= 0, z - 1 >= 0, z' >= 0
g_5(z, z') -{ 2 + 2·z' + 2·z'² + 2·z'³ + 2·z'⁴ }→ 1 + s9 + g_5(z - 1, z') :|: s9 >= 0, s9 <= 0, z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0] g_2: runtime: O(n2) [2·z + 2·z·z'], size: O(1) [0] f_2: runtime: O(n2) [1 + 2·z + 2·z2], size: O(1) [0] g_3: runtime: O(n3) [2·z + 2·z·z' + 2·z·z'2], size: O(1) [0] f_3: runtime: O(n3) [1 + 2·z + 2·z2 + 2·z3], size: O(1) [0] g_4: runtime: O(n4) [2·z + 2·z·z' + 2·z·z'2 + 2·z·z'3], size: O(1) [0] f_4: runtime: O(n4) [1 + 2·z + 2·z2 + 2·z3 + 2·z4], size: O(1) [0]

(71) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: g_5
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

(72) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 + 2·z + 2·z² }→ s1 :|: s1 >= 0, s1 <= 0, z >= 0
f_3(z) -{ 1 + 2·z + 2·z² + 2·z³ }→ s4 :|: s4 >= 0, s4 <= 0, z >= 0
f_4(z) -{ 1 + 2·z + 2·z² + 2·z³ + 2·z⁴ }→ s7 :|: s7 >= 0, s7 <= 0, z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2·z + 2·z·z' }→ 1 + s'' + s2 :|: s2 >= 0, s2 <= 0, s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 2·z + 2·z·z' + 2·z·z'² }→ 1 + s3 + s5 :|: s5 >= 0, s5 <= 0, s3 >= 0, s3 <= 0, z - 1 >= 0, z' >= 0
g_4(z, z') -{ 2·z + 2·z·z' + 2·z·z'² + 2·z·z'³ }→ 1 + s6 + s8 :|: s8 >= 0, s8 <= 0, s6 >= 0, s6 <= 0, z - 1 >= 0, z' >= 0
g_5(z, z') -{ 2 + 2·z' + 2·z'² + 2·z'³ + 2·z'⁴ }→ 1 + s9 + g_5(z - 1, z') :|: s9 >= 0, s9 <= 0, z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {g_5}, {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0] g_2: runtime: O(n2) [2·z + 2·z·z'], size: O(1) [0] f_2: runtime: O(n2) [1 + 2·z + 2·z2], size: O(1) [0] g_3: runtime: O(n3) [2·z + 2·z·z' + 2·z·z'2], size: O(1) [0] f_3: runtime: O(n3) [1 + 2·z + 2·z2 + 2·z3], size: O(1) [0] g_4: runtime: O(n4) [2·z + 2·z·z' + 2·z·z'2 + 2·z·z'3], size: O(1) [0] f_4: runtime: O(n4) [1 + 2·z + 2·z2 + 2·z3 + 2·z4], size: O(1) [0] g_5: runtime: ?, size: O(1) [0]

(73) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: g_5
after applying outer abstraction to obtain an ITS,
resulting in: O(n⁵) with polynomial bound: 2·z + 2·z·z' + 2·z·z'² + 2·z·z'³ + 2·z·z'⁴

(74) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 + 2·z + 2·z² }→ s1 :|: s1 >= 0, s1 <= 0, z >= 0
f_3(z) -{ 1 + 2·z + 2·z² + 2·z³ }→ s4 :|: s4 >= 0, s4 <= 0, z >= 0
f_4(z) -{ 1 + 2·z + 2·z² + 2·z³ + 2·z⁴ }→ s7 :|: s7 >= 0, s7 <= 0, z >= 0
f_5(z) -{ 1 }→ g_5(z, z) :|: z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2·z + 2·z·z' }→ 1 + s'' + s2 :|: s2 >= 0, s2 <= 0, s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 2·z + 2·z·z' + 2·z·z'² }→ 1 + s3 + s5 :|: s5 >= 0, s5 <= 0, s3 >= 0, s3 <= 0, z - 1 >= 0, z' >= 0
g_4(z, z') -{ 2·z + 2·z·z' + 2·z·z'² + 2·z·z'³ }→ 1 + s6 + s8 :|: s8 >= 0, s8 <= 0, s6 >= 0, s6 <= 0, z - 1 >= 0, z' >= 0
g_5(z, z') -{ 2 + 2·z' + 2·z'² + 2·z'³ + 2·z'⁴ }→ 1 + s9 + g_5(z - 1, z') :|: s9 >= 0, s9 <= 0, z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0] g_2: runtime: O(n2) [2·z + 2·z·z'], size: O(1) [0] f_2: runtime: O(n2) [1 + 2·z + 2·z2], size: O(1) [0] g_3: runtime: O(n3) [2·z + 2·z·z' + 2·z·z'2], size: O(1) [0] f_3: runtime: O(n3) [1 + 2·z + 2·z2 + 2·z3], size: O(1) [0] g_4: runtime: O(n4) [2·z + 2·z·z' + 2·z·z'2 + 2·z·z'3], size: O(1) [0] f_4: runtime: O(n4) [1 + 2·z + 2·z2 + 2·z3 + 2·z4], size: O(1) [0] g_5: runtime: O(n5) [2·z + 2·z·z' + 2·z·z'2 + 2·z·z'3 + 2·z·z'4], size: O(1) [0]

(75) ResultPropagationProof (UPPER BOUND(ID) transformation)

Applied inner abstraction using the recently inferred runtime/size bounds where possible.

(76) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 + 2·z + 2·z² }→ s1 :|: s1 >= 0, s1 <= 0, z >= 0
f_3(z) -{ 1 + 2·z + 2·z² + 2·z³ }→ s4 :|: s4 >= 0, s4 <= 0, z >= 0
f_4(z) -{ 1 + 2·z + 2·z² + 2·z³ + 2·z⁴ }→ s7 :|: s7 >= 0, s7 <= 0, z >= 0
f_5(z) -{ 1 + 2·z + 2·z² + 2·z³ + 2·z⁴ + 2·z⁵ }→ s10 :|: s10 >= 0, s10 <= 0, z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2·z + 2·z·z' }→ 1 + s'' + s2 :|: s2 >= 0, s2 <= 0, s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 2·z + 2·z·z' + 2·z·z'² }→ 1 + s3 + s5 :|: s5 >= 0, s5 <= 0, s3 >= 0, s3 <= 0, z - 1 >= 0, z' >= 0
g_4(z, z') -{ 2·z + 2·z·z' + 2·z·z'² + 2·z·z'³ }→ 1 + s6 + s8 :|: s8 >= 0, s8 <= 0, s6 >= 0, s6 <= 0, z - 1 >= 0, z' >= 0
g_5(z, z') -{ 2·z + 2·z·z' + 2·z·z'² + 2·z·z'³ + 2·z·z'⁴ }→ 1 + s9 + s11 :|: s11 >= 0, s11 <= 0, s9 >= 0, s9 <= 0, z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0] g_2: runtime: O(n2) [2·z + 2·z·z'], size: O(1) [0] f_2: runtime: O(n2) [1 + 2·z + 2·z2], size: O(1) [0] g_3: runtime: O(n3) [2·z + 2·z·z' + 2·z·z'2], size: O(1) [0] f_3: runtime: O(n3) [1 + 2·z + 2·z2 + 2·z3], size: O(1) [0] g_4: runtime: O(n4) [2·z + 2·z·z' + 2·z·z'2 + 2·z·z'3], size: O(1) [0] f_4: runtime: O(n4) [1 + 2·z + 2·z2 + 2·z3 + 2·z4], size: O(1) [0] g_5: runtime: O(n5) [2·z + 2·z·z' + 2·z·z'2 + 2·z·z'3 + 2·z·z'4], size: O(1) [0]

(77) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed SIZE bound using CoFloCo for: f_5
after applying outer abstraction to obtain an ITS,
resulting in: O(1) with polynomial bound: 0

(78) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 + 2·z + 2·z² }→ s1 :|: s1 >= 0, s1 <= 0, z >= 0
f_3(z) -{ 1 + 2·z + 2·z² + 2·z³ }→ s4 :|: s4 >= 0, s4 <= 0, z >= 0
f_4(z) -{ 1 + 2·z + 2·z² + 2·z³ + 2·z⁴ }→ s7 :|: s7 >= 0, s7 <= 0, z >= 0
f_5(z) -{ 1 + 2·z + 2·z² + 2·z³ + 2·z⁴ + 2·z⁵ }→ s10 :|: s10 >= 0, s10 <= 0, z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2·z + 2·z·z' }→ 1 + s'' + s2 :|: s2 >= 0, s2 <= 0, s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 2·z + 2·z·z' + 2·z·z'² }→ 1 + s3 + s5 :|: s5 >= 0, s5 <= 0, s3 >= 0, s3 <= 0, z - 1 >= 0, z' >= 0
g_4(z, z') -{ 2·z + 2·z·z' + 2·z·z'² + 2·z·z'³ }→ 1 + s6 + s8 :|: s8 >= 0, s8 <= 0, s6 >= 0, s6 <= 0, z - 1 >= 0, z' >= 0
g_5(z, z') -{ 2·z + 2·z·z' + 2·z·z'² + 2·z·z'³ + 2·z·z'⁴ }→ 1 + s9 + s11 :|: s11 >= 0, s11 <= 0, s9 >= 0, s9 <= 0, z - 1 >= 0, z' >= 0

Function symbols to be analyzed: {f_5}
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0] g_2: runtime: O(n2) [2·z + 2·z·z'], size: O(1) [0] f_2: runtime: O(n2) [1 + 2·z + 2·z2], size: O(1) [0] g_3: runtime: O(n3) [2·z + 2·z·z' + 2·z·z'2], size: O(1) [0] f_3: runtime: O(n3) [1 + 2·z + 2·z2 + 2·z3], size: O(1) [0] g_4: runtime: O(n4) [2·z + 2·z·z' + 2·z·z'2 + 2·z·z'3], size: O(1) [0] f_4: runtime: O(n4) [1 + 2·z + 2·z2 + 2·z3 + 2·z4], size: O(1) [0] g_5: runtime: O(n5) [2·z + 2·z·z' + 2·z·z'2 + 2·z·z'3 + 2·z·z'4], size: O(1) [0] f_5: runtime: ?, size: O(1) [0]

(79) IntTrsBoundProof (UPPER BOUND(ID) transformation)

Computed RUNTIME bound using KoAT for: f_5
after applying outer abstraction to obtain an ITS,
resulting in: O(n⁵) with polynomial bound: 1 + 2·z + 2·z² + 2·z³ + 2·z⁴ + 2·z⁵

(80) Obligation:

Complexity RNTS consisting of the following rules:

f_0(z) -{ 1 }→ 0 :|: z >= 0
f_1(z) -{ 1 + 2·z }→ s :|: s >= 0, s <= 0, z >= 0
f_2(z) -{ 1 + 2·z + 2·z² }→ s1 :|: s1 >= 0, s1 <= 0, z >= 0
f_3(z) -{ 1 + 2·z + 2·z² + 2·z³ }→ s4 :|: s4 >= 0, s4 <= 0, z >= 0
f_4(z) -{ 1 + 2·z + 2·z² + 2·z³ + 2·z⁴ }→ s7 :|: s7 >= 0, s7 <= 0, z >= 0
f_5(z) -{ 1 + 2·z + 2·z² + 2·z³ + 2·z⁴ + 2·z⁵ }→ s10 :|: s10 >= 0, s10 <= 0, z >= 0
g_1(z, z') -{ 2·z }→ 1 + 0 + s' :|: s' >= 0, s' <= 0, z - 1 >= 0, z' >= 0
g_2(z, z') -{ 2·z + 2·z·z' }→ 1 + s'' + s2 :|: s2 >= 0, s2 <= 0, s'' >= 0, s'' <= 0, z - 1 >= 0, z' >= 0
g_3(z, z') -{ 2·z + 2·z·z' + 2·z·z'² }→ 1 + s3 + s5 :|: s5 >= 0, s5 <= 0, s3 >= 0, s3 <= 0, z - 1 >= 0, z' >= 0
g_4(z, z') -{ 2·z + 2·z·z' + 2·z·z'² + 2·z·z'³ }→ 1 + s6 + s8 :|: s8 >= 0, s8 <= 0, s6 >= 0, s6 <= 0, z - 1 >= 0, z' >= 0
g_5(z, z') -{ 2·z + 2·z·z' + 2·z·z'² + 2·z·z'³ + 2·z·z'⁴ }→ 1 + s9 + s11 :|: s11 >= 0, s11 <= 0, s9 >= 0, s9 <= 0, z - 1 >= 0, z' >= 0

Function symbols to be analyzed:
Previous analysis results are:

f_0: runtime: O(1) [1], size: O(1) [0] g_1: runtime: O(n1) [2·z], size: O(1) [0] f_1: runtime: O(n1) [1 + 2·z], size: O(1) [0] g_2: runtime: O(n2) [2·z + 2·z·z'], size: O(1) [0] f_2: runtime: O(n2) [1 + 2·z + 2·z2], size: O(1) [0] g_3: runtime: O(n3) [2·z + 2·z·z' + 2·z·z'2], size: O(1) [0] f_3: runtime: O(n3) [1 + 2·z + 2·z2 + 2·z3], size: O(1) [0] g_4: runtime: O(n4) [2·z + 2·z·z' + 2·z·z'2 + 2·z·z'3], size: O(1) [0] f_4: runtime: O(n4) [1 + 2·z + 2·z2 + 2·z3 + 2·z4], size: O(1) [0] g_5: runtime: O(n5) [2·z + 2·z·z' + 2·z·z'2 + 2·z·z'3 + 2·z·z'4], size: O(1) [0] f_5: runtime: O(n5) [1 + 2·z + 2·z2 + 2·z3 + 2·z4 + 2·z5], size: O(1) [0]

(81) FinalProof (EQUIVALENT transformation)

Computed overall runtime complexity

(82) BOUNDS(1, n^5)